Nuprl Lemma : eqmod_transitivity
2,24
postcript
pdf
m
,
a
,
b
,
c
:
. (
a
=
b
mod
m
)
(
b
=
c
mod
m
)
(
a
=
c
mod
m
)
latex
Definitions
a
=
b
mod
m
,
P
Q
,
b
|
a
,
x
:
A
.
B
(
x
)
,
t
T
,
T
,
True
,
Prop
Lemmas
true
wf
,
squash
wf
,
divisor
of
sum
,
divides
wf
origin
m, a, b, c:
. (a = b mod m) 
(b = c mod m) (a = c mod m) m, a, b, c:. (a = b mod m) (b = c mod m) (a = c mod m) Qx:A. B(x)
T
T